Runtime Complexity (innermost) proof of /tmp/tmpCDzxvg/nolexicord.xml

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).

0 CpxRelTRS

↳1 RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 CpxWeightedTrs

↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CpxTypedWeightedTrs

↳5 CompletionProof (UPPER BOUND(ID), 0 ms)

↳6 CpxTypedWeightedCompleteTrs

↳7 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳8 CpxTypedWeightedCompleteTrs

↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 15 ms)

↳10 CpxRNTS

↳11 SimplificationProof (BOTH BOUNDS(ID, ID), 21 ms)

↳12 CpxRNTS

↳13 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 0 ms)

↳14 CpxRNTS

↳15 IntTrsBoundProof (UPPER BOUND(ID), 61 ms)

↳16 CpxRNTS

↳17 IntTrsBoundProof (UPPER BOUND(ID), 37 ms)

↳18 CpxRNTS

↳19 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳20 CpxRNTS

↳21 IntTrsBoundProof (UPPER BOUND(ID), 466 ms)

↳22 CpxRNTS

↳23 IntTrsBoundProof (UPPER BOUND(ID), 12 ms)

↳24 CpxRNTS

↳25 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳26 CpxRNTS

↳27 IntTrsBoundProof (UPPER BOUND(ID), 453 ms)

↳28 CpxRNTS

↳29 IntTrsBoundProof (UPPER BOUND(ID), 10 ms)

↳30 CpxRNTS

↳31 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳32 CpxRNTS

↳33 IntTrsBoundProof (UPPER BOUND(ID), 10.2 s)

↳34 CpxRNTS

↳35 IntTrsBoundProof (UPPER BOUND(ID), 5206 ms)

↳36 CpxRNTS

↳37 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳38 CpxRNTS

↳39 IntTrsBoundProof (UPPER BOUND(ID), 314 ms)

↳40 CpxRNTS

↳41 IntTrsBoundProof (UPPER BOUND(ID), 78 ms)

↳42 CpxRNTS

↳43 FinalProof (⇔, 0 ms)

↳44 BOUNDS(1, n^1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).

The TRS R consists of the following rules:

nolexicord(Nil, b1, a2, b2, a3, b3) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))))))))))))))))))))))))))))
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) → nolexicord[Ite][False][Ite](eqNatList(Cons(x, xs), b1), Cons(x, xs), b1, a2, b2, a3, b3)
number42 → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))))))))))))))))))))))))))))
goal(a1, b1, a2, b2, a3, b3) → nolexicord(a1, b1, a2, b2, a3, b3)

The (relative) TRS S consists of the following rules:

!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
nolexicord[Ite][False][Ite](False, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs)) → nolexicord(xs', xs', xs', xs', xs', xs)
nolexicord[Ite][False][Ite](True, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs), Cons(x', xs')) → nolexicord(xs', xs', xs', xs', xs', xs)

Rewrite Strategy: INNERMOST

(1) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed relative TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).

The TRS R consists of the following rules:

nolexicord(Nil, b1, a2, b2, a3, b3) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) [1]
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) [1]
eqNatList(Cons(x, xs), Nil) → False [1]
eqNatList(Nil, Cons(y, ys)) → False [1]
eqNatList(Nil, Nil) → True [1]
nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) → nolexicord[Ite][False][Ite](eqNatList(Cons(x, xs), b1), Cons(x, xs), b1, a2, b2, a3, b3) [1]
number42 → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) [1]
goal(a1, b1, a2, b2, a3, b3) → nolexicord(a1, b1, a2, b2, a3, b3) [1]
!EQ(S(x), S(y)) → !EQ(x, y) [0]
!EQ(0, S(y)) → False [0]
!EQ(S(x), 0) → False [0]
!EQ(0, 0) → True [0]
nolexicord[Ite][False][Ite](False, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs)) → nolexicord(xs', xs', xs', xs', xs', xs) [0]
nolexicord[Ite][False][Ite](True, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs), Cons(x', xs')) → nolexicord(xs', xs', xs', xs', xs', xs) [0]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

nolexicord(Nil, b1, a2, b2, a3, b3) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) [1]
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) [1]
eqNatList(Cons(x, xs), Nil) → False [1]
eqNatList(Nil, Cons(y, ys)) → False [1]
eqNatList(Nil, Nil) → True [1]
nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) → nolexicord[Ite][False][Ite](eqNatList(Cons(x, xs), b1), Cons(x, xs), b1, a2, b2, a3, b3) [1]
number42 → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) [1]
goal(a1, b1, a2, b2, a3, b3) → nolexicord(a1, b1, a2, b2, a3, b3) [1]
!EQ(S(x), S(y)) → !EQ(x, y) [0]
!EQ(0, S(y)) → False [0]
!EQ(S(x), 0) → False [0]
!EQ(0, 0) → True [0]
nolexicord[Ite][False][Ite](False, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs)) → nolexicord(xs', xs', xs', xs', xs', xs) [0]
nolexicord[Ite][False][Ite](True, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs), Cons(x', xs')) → nolexicord(xs', xs', xs', xs', xs', xs) [0]

The TRS has the following type information:

nolexicord :: Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0
Nil :: Nil:Cons:S:0
Cons :: Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0
eqNatList :: Nil:Cons:S:0 → Nil:Cons:S:0 → eqNatList[Match][Cons][Match][Cons][Ite]:False:True
eqNatList[Match][Cons][Match][Cons][Ite] :: eqNatList[Match][Cons][Match][Cons][Ite]:False:True → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → eqNatList[Match][Cons][Match][Cons][Ite]:False:True
!EQ :: Nil:Cons:S:0 → Nil:Cons:S:0 → eqNatList[Match][Cons][Match][Cons][Ite]:False:True
False :: eqNatList[Match][Cons][Match][Cons][Ite]:False:True
True :: eqNatList[Match][Cons][Match][Cons][Ite]:False:True
nolexicord[Ite][False][Ite] :: eqNatList[Match][Cons][Match][Cons][Ite]:False:True → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0
number42 :: Nil:Cons:S:0
goal :: Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0 → Nil:Cons:S:0
S :: Nil:Cons:S:0 → Nil:Cons:S:0
0 :: Nil:Cons:S:0

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

nolexicord
number42
goal

eqNatList
!EQ
nolexicord[Ite][False][Ite]

Due to the following rules being added:

!EQ(v0, v1) → null_!EQ [0]
nolexicord[Ite][False][Ite](v0, v1, v2, v3, v4, v5, v6) → null_nolexicord[Ite][False][Ite] [0]
eqNatList(v0, v1) → null_eqNatList [0]

And the following fresh constants:

null_!EQ, null_nolexicord[Ite][False][Ite], null_eqNatList

(6) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

nolexicord(Nil, b1, a2, b2, a3, b3) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) [1]
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) [1]
eqNatList(Cons(x, xs), Nil) → False [1]
eqNatList(Nil, Cons(y, ys)) → False [1]
eqNatList(Nil, Nil) → True [1]
nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) → nolexicord[Ite][False][Ite](eqNatList(Cons(x, xs), b1), Cons(x, xs), b1, a2, b2, a3, b3) [1]
number42 → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) [1]
goal(a1, b1, a2, b2, a3, b3) → nolexicord(a1, b1, a2, b2, a3, b3) [1]
!EQ(S(x), S(y)) → !EQ(x, y) [0]
!EQ(0, S(y)) → False [0]
!EQ(S(x), 0) → False [0]
!EQ(0, 0) → True [0]
nolexicord[Ite][False][Ite](False, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs)) → nolexicord(xs', xs', xs', xs', xs', xs) [0]
nolexicord[Ite][False][Ite](True, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs), Cons(x', xs')) → nolexicord(xs', xs', xs', xs', xs', xs) [0]
!EQ(v0, v1) → null_!EQ [0]
nolexicord[Ite][False][Ite](v0, v1, v2, v3, v4, v5, v6) → null_nolexicord[Ite][False][Ite] [0]
eqNatList(v0, v1) → null_eqNatList [0]

The TRS has the following type information:

nolexicord :: Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite]
Nil :: Nil:Cons:S:0:null_nolexicord[Ite][False][Ite]
Cons :: Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite]
eqNatList :: Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → eqNatList[Match][Cons][Match][Cons][Ite]:False:True:null_!EQ:null_eqNatList
eqNatList[Match][Cons][Match][Cons][Ite] :: eqNatList[Match][Cons][Match][Cons][Ite]:False:True:null_!EQ:null_eqNatList → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → eqNatList[Match][Cons][Match][Cons][Ite]:False:True:null_!EQ:null_eqNatList
!EQ :: Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → eqNatList[Match][Cons][Match][Cons][Ite]:False:True:null_!EQ:null_eqNatList
False :: eqNatList[Match][Cons][Match][Cons][Ite]:False:True:null_!EQ:null_eqNatList
True :: eqNatList[Match][Cons][Match][Cons][Ite]:False:True:null_!EQ:null_eqNatList
nolexicord[Ite][False][Ite] :: eqNatList[Match][Cons][Match][Cons][Ite]:False:True:null_!EQ:null_eqNatList → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite]
number42 :: Nil:Cons:S:0:null_nolexicord[Ite][False][Ite]
goal :: Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite]
S :: Nil:Cons:S:0:null_nolexicord[Ite][False][Ite] → Nil:Cons:S:0:null_nolexicord[Ite][False][Ite]
0 :: Nil:Cons:S:0:null_nolexicord[Ite][False][Ite]
null_!EQ :: eqNatList[Match][Cons][Match][Cons][Ite]:False:True:null_!EQ:null_eqNatList
null_nolexicord[Ite][False][Ite] :: Nil:Cons:S:0:null_nolexicord[Ite][False][Ite]
null_eqNatList :: eqNatList[Match][Cons][Match][Cons][Ite]:False:True:null_!EQ:null_eqNatList

Rewrite Strategy: INNERMOST

(7) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

nolexicord(Nil, b1, a2, b2, a3, b3) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) [1]
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) [1]
eqNatList(Cons(x, xs), Nil) → False [1]
eqNatList(Nil, Cons(y, ys)) → False [1]
eqNatList(Nil, Nil) → True [1]
nolexicord(Cons(x, xs), Cons(y', ys'), a2, b2, a3, b3) → nolexicord[Ite][False][Ite](eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y'), y', ys', x, xs), Cons(x, xs), Cons(y', ys'), a2, b2, a3, b3) [2]
nolexicord(Cons(x, xs), Nil, a2, b2, a3, b3) → nolexicord[Ite][False][Ite](False, Cons(x, xs), Nil, a2, b2, a3, b3) [2]
nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) → nolexicord[Ite][False][Ite](null_eqNatList, Cons(x, xs), b1, a2, b2, a3, b3) [1]
number42 → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) [1]
goal(a1, b1, a2, b2, a3, b3) → nolexicord(a1, b1, a2, b2, a3, b3) [1]
!EQ(S(x), S(y)) → !EQ(x, y) [0]
!EQ(0, S(y)) → False [0]
!EQ(S(x), 0) → False [0]
!EQ(0, 0) → True [0]
nolexicord[Ite][False][Ite](False, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs)) → nolexicord(xs', xs', xs', xs', xs', xs) [0]
nolexicord[Ite][False][Ite](True, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs), Cons(x', xs')) → nolexicord(xs', xs', xs', xs', xs', xs) [0]
!EQ(v0, v1) → null_!EQ [0]
nolexicord[Ite][False][Ite](v0, v1, v2, v3, v4, v5, v6) → null_nolexicord[Ite][False][Ite] [0]
eqNatList(v0, v1) → null_eqNatList [0]

The TRS has the following type information:

Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

Nil => 1
False => 0
True => 1
0 => 0
null_!EQ => 0
null_nolexicord[Ite][False][Ite] => 0
null_eqNatList => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' = 1 + y, y >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: x >= 0, z = 1 + x, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
!EQ(z, z') -{ 0 }→ !EQ(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
eqNatList(z, z') -{ 1 }→ 1 + !EQ(x, y) + y + ys + x + xs :|: z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(a1, b1, a2, b2, a3, b3) :|: b2 >= 0, z = a1, a1 >= 0, a2 >= 0, b1 >= 0, z1 = b2, z2 = a3, z' = b1, z3 = b3, z'' = a2, a3 >= 0, b3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, b1, a2, b2, a3, b3) :|: xs >= 0, a2 >= 0, b1 >= 0, z2 = a3, z' = b1, z3 = b3, z'' = a2, a3 >= 0, b3 >= 0, z = 1 + x + xs, b2 >= 0, x >= 0, z1 = b2
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, a2, b2, a3, b3) :|: z = 1 + x + xs, xs >= 0, b2 >= 0, a2 >= 0, x >= 0, z1 = b2, z' = 1, z2 = a3, z3 = b3, z'' = a2, a3 >= 0, b3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + !EQ(x, y') + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', a2, b2, a3, b3) :|: xs >= 0, a2 >= 0, ys' >= 0, z2 = a3, z3 = b3, z'' = a2, a3 >= 0, b3 >= 0, z = 1 + x + xs, b2 >= 0, z' = 1 + y' + ys', x >= 0, z1 = b2, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: b2 >= 0, a2 >= 0, b1 >= 0, z = 1, z1 = b2, z2 = a3, z' = b1, z3 = b3, z'' = a2, a3 >= 0, b3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, v6 >= 0, z'' = v2, v1 >= 0, v5 >= 0, z = v0, z' = v1, z2 = v4, v2 >= 0, v3 >= 0, z3 = v5, v4 >= 0, z4 = v6
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

(11) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(12) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
!EQ(z, z') -{ 0 }→ !EQ(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + !EQ(x, y) + y + ys + x + xs :|: z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(z, z', z'', z1, z2, z3) :|: z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, z', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, z'', z1, z2, z3) :|: z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + !EQ(x, y') + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

(13) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ number42 }
{ !EQ }
{ eqNatList }
{ nolexicord[Ite][False][Ite], nolexicord }
{ goal }

(14) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
!EQ(z, z') -{ 0 }→ !EQ(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + !EQ(x, y) + y + ys + x + xs :|: z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(z, z', z'', z1, z2, z3) :|: z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, z', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, z'', z1, z2, z3) :|: z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + !EQ(x, y') + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {number42}, {!EQ}, {eqNatList}, {nolexicord[Ite][False][Ite],nolexicord}, {goal}

(15) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: number42
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 85

(16) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
!EQ(z, z') -{ 0 }→ !EQ(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + !EQ(x, y) + y + ys + x + xs :|: z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(z, z', z'', z1, z2, z3) :|: z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, z', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, z'', z1, z2, z3) :|: z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + !EQ(x, y') + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {number42}, {!EQ}, {eqNatList}, {nolexicord[Ite][False][Ite],nolexicord}, {goal}
Previous analysis results are:

number42: runtime: ?, size: O(1) [85]

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: number42
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(18) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
!EQ(z, z') -{ 0 }→ !EQ(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + !EQ(x, y) + y + ys + x + xs :|: z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(z, z', z'', z1, z2, z3) :|: z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, z', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, z'', z1, z2, z3) :|: z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + !EQ(x, y') + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {!EQ}, {eqNatList}, {nolexicord[Ite][False][Ite],nolexicord}, {goal}
Previous analysis results are:

number42: runtime: O(1) [1], size: O(1) [85]

(19) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(20) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
!EQ(z, z') -{ 0 }→ !EQ(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + !EQ(x, y) + y + ys + x + xs :|: z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(z, z', z'', z1, z2, z3) :|: z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, z', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, z'', z1, z2, z3) :|: z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + !EQ(x, y') + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {!EQ}, {eqNatList}, {nolexicord[Ite][False][Ite],nolexicord}, {goal}
Previous analysis results are:

number42: runtime: O(1) [1], size: O(1) [85]

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: !EQ
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(22) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
!EQ(z, z') -{ 0 }→ !EQ(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + !EQ(x, y) + y + ys + x + xs :|: z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(z, z', z'', z1, z2, z3) :|: z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, z', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, z'', z1, z2, z3) :|: z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + !EQ(x, y') + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {!EQ}, {eqNatList}, {nolexicord[Ite][False][Ite],nolexicord}, {goal}
Previous analysis results are:

number42: runtime: O(1) [1], size: O(1) [85]
!EQ: runtime: ?, size: O(1) [1]

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: !EQ
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(24) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
!EQ(z, z') -{ 0 }→ !EQ(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + !EQ(x, y) + y + ys + x + xs :|: z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(z, z', z'', z1, z2, z3) :|: z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, z', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, z'', z1, z2, z3) :|: z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + !EQ(x, y') + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {eqNatList}, {nolexicord[Ite][False][Ite],nolexicord}, {goal}
Previous analysis results are:

number42: runtime: O(1) [1], size: O(1) [85]
!EQ: runtime: O(1) [0], size: O(1) [1]

(25) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(26) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ s'' :|: s'' >= 0, s'' <= 1, z - 1 >= 0, z' - 1 >= 0
!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + s + y + ys + x + xs :|: s >= 0, s <= 1, z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(z, z', z'', z1, z2, z3) :|: z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, z', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, z'', z1, z2, z3) :|: z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + s' + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', z'', z1, z2, z3) :|: s' >= 0, s' <= 1, xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {eqNatList}, {nolexicord[Ite][False][Ite],nolexicord}, {goal}
Previous analysis results are:

number42: runtime: O(1) [1], size: O(1) [85]
!EQ: runtime: O(1) [0], size: O(1) [1]

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: eqNatList
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

(28) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ s'' :|: s'' >= 0, s'' <= 1, z - 1 >= 0, z' - 1 >= 0
!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + s + y + ys + x + xs :|: s >= 0, s <= 1, z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(z, z', z'', z1, z2, z3) :|: z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, z', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, z'', z1, z2, z3) :|: z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + s' + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', z'', z1, z2, z3) :|: s' >= 0, s' <= 1, xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {eqNatList}, {nolexicord[Ite][False][Ite],nolexicord}, {goal}
Previous analysis results are:

number42: runtime: O(1) [1], size: O(1) [85]
!EQ: runtime: O(1) [0], size: O(1) [1]
eqNatList: runtime: ?, size: O(n¹) [z + z']

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: eqNatList
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(30) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ s'' :|: s'' >= 0, s'' <= 1, z - 1 >= 0, z' - 1 >= 0
!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + s + y + ys + x + xs :|: s >= 0, s <= 1, z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(z, z', z'', z1, z2, z3) :|: z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, z', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, z'', z1, z2, z3) :|: z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + s' + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', z'', z1, z2, z3) :|: s' >= 0, s' <= 1, xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {nolexicord[Ite][False][Ite],nolexicord}, {goal}
Previous analysis results are:

number42: runtime: O(1) [1], size: O(1) [85]
!EQ: runtime: O(1) [0], size: O(1) [1]
eqNatList: runtime: O(1) [1], size: O(n¹) [z + z']

(31) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(32) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ s'' :|: s'' >= 0, s'' <= 1, z - 1 >= 0, z' - 1 >= 0
!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + s + y + ys + x + xs :|: s >= 0, s <= 1, z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(z, z', z'', z1, z2, z3) :|: z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, z', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, z'', z1, z2, z3) :|: z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + s' + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', z'', z1, z2, z3) :|: s' >= 0, s' <= 1, xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {nolexicord[Ite][False][Ite],nolexicord}, {goal}
Previous analysis results are:

number42: runtime: O(1) [1], size: O(1) [85]
!EQ: runtime: O(1) [0], size: O(1) [1]
eqNatList: runtime: O(1) [1], size: O(n¹) [z + z']

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: nolexicord[Ite][False][Ite]
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 85

Computed SIZE bound using CoFloCo for: nolexicord
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 85

(34) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ s'' :|: s'' >= 0, s'' <= 1, z - 1 >= 0, z' - 1 >= 0
!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + s + y + ys + x + xs :|: s >= 0, s <= 1, z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(z, z', z'', z1, z2, z3) :|: z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, z', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, z'', z1, z2, z3) :|: z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + s' + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', z'', z1, z2, z3) :|: s' >= 0, s' <= 1, xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {nolexicord[Ite][False][Ite],nolexicord}, {goal}
Previous analysis results are:

number42: runtime: O(1) [1], size: O(1) [85]
!EQ: runtime: O(1) [0], size: O(1) [1]
eqNatList: runtime: O(1) [1], size: O(n¹) [z + z']
nolexicord[Ite][False][Ite]: runtime: ?, size: O(1) [85]
nolexicord: runtime: ?, size: O(1) [85]

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: nolexicord[Ite][False][Ite]
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 5 + z3 + z4

Computed RUNTIME bound using CoFloCo for: nolexicord
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 7 + z2 + z3

(36) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ s'' :|: s'' >= 0, s'' <= 1, z - 1 >= 0, z' - 1 >= 0
!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + s + y + ys + x + xs :|: s >= 0, s <= 1, z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord(z, z', z'', z1, z2, z3) :|: z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, z', z'', z1, z2, z3) :|: xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](0, 1 + x + xs, 1, z'', z1, z2, z3) :|: z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 2 }→ nolexicord[Ite][False][Ite](1 + s' + y' + ys' + x + xs, 1 + x + xs, 1 + y' + ys', z'', z1, z2, z3) :|: s' >= 0, s' <= 1, xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ nolexicord(xs', xs', xs', xs', xs', xs) :|: xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {goal}
Previous analysis results are:

number42: runtime: O(1) [1], size: O(1) [85]
!EQ: runtime: O(1) [0], size: O(1) [1]
eqNatList: runtime: O(1) [1], size: O(n¹) [z + z']
nolexicord[Ite][False][Ite]: runtime: O(n¹) [5 + z3 + z4], size: O(1) [85]
nolexicord: runtime: O(n¹) [7 + z2 + z3], size: O(1) [85]

(37) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(38) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ s'' :|: s'' >= 0, s'' <= 1, z - 1 >= 0, z' - 1 >= 0
!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + s + y + ys + x + xs :|: s >= 0, s <= 1, z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 8 + z2 + z3 }→ s4 :|: s4 >= 0, s4 <= 85, z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 7 + z2 + z3 }→ s1 :|: s1 >= 0, s1 <= 85, s' >= 0, s' <= 1, xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 7 + z2 + z3 }→ s2 :|: s2 >= 0, s2 <= 85, z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 6 + z2 + z3 }→ s3 :|: s3 >= 0, s3 <= 85, xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 7 + xs + xs' }→ s5 :|: s5 >= 0, s5 <= 85, xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 7 + xs + xs' }→ s6 :|: s6 >= 0, s6 <= 85, xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {goal}
Previous analysis results are:

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: goal
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 85

(40) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ s'' :|: s'' >= 0, s'' <= 1, z - 1 >= 0, z' - 1 >= 0
!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + s + y + ys + x + xs :|: s >= 0, s <= 1, z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 8 + z2 + z3 }→ s4 :|: s4 >= 0, s4 <= 85, z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 7 + z2 + z3 }→ s1 :|: s1 >= 0, s1 <= 85, s' >= 0, s' <= 1, xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 7 + z2 + z3 }→ s2 :|: s2 >= 0, s2 <= 85, z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 6 + z2 + z3 }→ s3 :|: s3 >= 0, s3 <= 85, xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 7 + xs + xs' }→ s5 :|: s5 >= 0, s5 <= 85, xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 7 + xs + xs' }→ s6 :|: s6 >= 0, s6 <= 85, xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed: {goal}
Previous analysis results are:

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: goal
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 8 + z2 + z3

(42) Obligation:

Complexity RNTS consisting of the following rules:

!EQ(z, z') -{ 0 }→ s'' :|: s'' >= 0, s'' <= 1, z - 1 >= 0, z' - 1 >= 0
!EQ(z, z') -{ 0 }→ 1 :|: z = 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z' - 1 >= 0, z = 0
!EQ(z, z') -{ 0 }→ 0 :|: z - 1 >= 0, z' = 0
!EQ(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 :|: z = 1, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1 + x + xs, xs >= 0, x >= 0, z' = 1
eqNatList(z, z') -{ 1 }→ 0 :|: z = 1, ys >= 0, y >= 0, z' = 1 + y + ys
eqNatList(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
eqNatList(z, z') -{ 1 }→ 1 + s + y + ys + x + xs :|: s >= 0, s <= 1, z = 1 + x + xs, xs >= 0, ys >= 0, x >= 0, y >= 0, z' = 1 + y + ys
goal(z, z', z'', z1, z2, z3) -{ 8 + z2 + z3 }→ s4 :|: s4 >= 0, s4 <= 85, z1 >= 0, z >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 7 + z2 + z3 }→ s1 :|: s1 >= 0, s1 <= 85, s' >= 0, s' <= 1, xs >= 0, z'' >= 0, ys' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, z' = 1 + y' + ys', x >= 0, y' >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 7 + z2 + z3 }→ s2 :|: s2 >= 0, s2 <= 85, z = 1 + x + xs, xs >= 0, z1 >= 0, z'' >= 0, x >= 0, z' = 1, z2 >= 0, z3 >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 6 + z2 + z3 }→ s3 :|: s3 >= 0, s3 <= 85, xs >= 0, z'' >= 0, z' >= 0, z2 >= 0, z3 >= 0, z = 1 + x + xs, z1 >= 0, x >= 0
nolexicord(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|: z1 >= 0, z'' >= 0, z' >= 0, z = 1, z2 >= 0, z3 >= 0
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 7 + xs + xs' }→ s5 :|: s5 >= 0, s5 <= 85, xs >= 0, x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z4 = 1 + x + xs, z3 = 1 + x' + xs', z = 0, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 7 + xs + xs' }→ s6 :|: s6 >= 0, s6 <= 85, xs >= 0, z = 1, z4 = 1 + x' + xs', x' >= 0, xs' >= 0, x >= 0, z'' = 1 + x' + xs', z' = 1 + x' + xs', z3 = 1 + x + xs, z2 = 1 + x' + xs', z1 = 1 + x' + xs'
nolexicord[Ite][False][Ite](z, z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z >= 0, z4 >= 0, z' >= 0, z3 >= 0, z'' >= 0, z1 >= 0, z2 >= 0
number42 -{ 1 }→ 1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + (1 + 1 + 1))))))))))))))))))))))))))))))))))))))))) :|:

Function symbols to be analyzed:
Previous analysis results are:

(43) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(0) Obligation:

(1) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CompletionProof (UPPER BOUND(ID) transformation)

(6) Obligation:

(7) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

(10) Obligation:

(11) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

(12) Obligation:

(13) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

(14) Obligation:

(15) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(16) Obligation:

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(18) Obligation:

(19) ResultPropagationProof (UPPER BOUND(ID) transformation)

(20) Obligation:

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(22) Obligation:

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(24) Obligation:

(25) ResultPropagationProof (UPPER BOUND(ID) transformation)

(26) Obligation:

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(28) Obligation:

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(30) Obligation:

(31) ResultPropagationProof (UPPER BOUND(ID) transformation)

(32) Obligation:

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(34) Obligation:

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(36) Obligation:

(37) ResultPropagationProof (UPPER BOUND(ID) transformation)

(38) Obligation:

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(40) Obligation:

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(42) Obligation:

(43) FinalProof (EQUIVALENT transformation)

(44) BOUNDS(1, n^1)